
\chapter{Выводы и результаты}

\ifpdf

    \graphicspath{{Chapter2/Chapter2Figs/PNG/}{Chapter2/Chapter2Figs/PDF/}{Chapter2/Chapter2Figs/}}

\else

    \graphicspath{{Chapter2/Chapter2Figs/EPS/}{Chapter2/Chapter2Figs/}}

\fi

% ------------------------------------------------------------------------

\section{Результаты}

\subsection{Просто типизированное $\lambda$-исчисление}

В Разделе 2.2 была сформулирована цель работы и поставлены соответствующие задачи. В данной подразделе будут описаны полученные результаты для Просто типизированное $\lambda$-исчисления. \\
Далее будут изложены результаты каждой из задач, а затем сделаны соответствующие выводы. \\
\textbf{1. Реализовать систему пошаговой редукции.} \hspace*{\fill} \\
Как и для любой формальной системы для начала нам необходимо вспомнить определение в абстрактном синтаксисе(раздел 1.2):
\begin{center}
e := v|e_{1}e_{2}|$\lambda$x.e
\end{center}
\hspace*{\fill} \\
Теперь перепишем его в виде типа данных языка Haskell. 
\begin{lstlisting}
data Expr = Var String | App Expr Expr | Abs String Expr deriving (Eq, Ord)
\end{lstlisting}
Далее из раздела 1.1 следует что формально мы можем определить свободные переменные $\lambda$-выражения как\\
\begin{center}
FV(x) = \{x\} \\
FV(MN) = FV(M) $\cup$ FV(N) \\
FV($\lambda$x.M) = FV(M) $\setminus$ \{x\} 
\end{center} 

Вернемся к написанию кода: 
\begin{lstlisting}
occursFree :: Name -> Expr -> Bool 
occursFree x = foldExp (x==) (||) (\y r->x/=y && r) 
\end{lstlisting}

Данный метод осуществляет проверку принадлежности переменной x множеству свободных переменных.\\
Затем часто необходимо произвести замену соответствующих переменных. В разделе 1.1 были введены обозначения:
\begin{center}
M[x:=e] $\Leftrightarrow$ замене всех свободных вхождений x в M e.
\end{center}
Для углублённого изучения данного алгоритма можно порекомендовать работы [1] и [2], а так же статью [11]. \\

Помним что при $\beta$-редукции выражение ($\lambda$x.M)N заменяется на M[x:=N], которое означает замещение всех свободных переменных x на N. 
Ниже приведен код для $\beta$-редукции. 

\begin{lstlisting}

beta :: Expr -> Expr -> Maybe Expr
beta (Abs x e) e2 = Just (subst e e2 x)
beta _         _  = Nothing

\end{lstlisting}

Как было показано в разделе 1, помимо этого нам необходимо уметь генерировать имена переменных, которые не используется в данный момент.

\begin{lstlisting}
fresh :: Expr -> Name
fresh e = head (strings \\ ("":ids e)) 
    where strings  = "":[a:as | as <- strings, a <- ['a'..'z']]
\end{lstlisting}

Помимо этого была реализована подсистема строкового ввода-вывода термов.\\
\hspace*{\fill} \\

\textbf{2. Реализовать систему вывода типов.} \hspace*{\fill} \\
Для реализации системы выводы типов был построен тип, аналогичный задаче 1, т.е.
\begin{lstlisting}
data Expr = Var String | App Expr Expr | Abs String Expr deriving (Eq, Ord)
\end{lstlisting}
Затем нам необходимо ввести тип Type, который описывает типы, сопоставляемые $\lambda$-термам. Для этого была выбрана структура:\\
\begin{lstlisting}
data Type = Const | TyVar String | Arrow Type Type deriving (Eq, Ord)
\end{lstlisting}

Затем нам необходим метод, который возвращает пару, первый элемент которой это новое состояние(в него должен быть включен тип обрабатываемого на данный момент выражения), а второй элемент - это список возможных идентификаторов типовых переменных. Для этого была реализована функция inferType, тип которой представлен ниже:

\begin{lstlisting}
inferType :: Expr -> [String] -> Environment -> Either String (Environment, [String]) 
\end{lstlisting}

Теперь необходимо реализовать функцию для унификации типов unifyTypes и предикат для проверки типов на совместимость areTypesCompatible. Очевидно, что первая функция должна получать на вход два типа — первый необходимо унифицировать вторым. Типовая константа унифицируется с типовой константой, при этом изменений в окружение не вносится. Типовая переменная может быть унифицирована любым типом при помощи подстановки вместо типовой переменной этого типа во всех типовых выражениях, находящихся в окружении. Она определена ниже:

\begin{lstlisting}

unifyTypes :: (Type, Type) -> Environment -> Either String Environment 
unifyTypes (Const, Const) env               = return env
unifyTypes (TyVar n, t) env                 = return $ Map.map (substituteTyVar n t) env
unifyTypes (Arrow t1 t2, Arrow t1' t2') env = do env' <- unifyTypes (t1, t1') env
                                                 unifyTypes (t2, t2') env'
unifyTypes (t1, t2) _ = fail ("ERROR: Can't unify type (" ++ show t1 ++ ") with (" ++ show t2 ++ ").")

\end{lstlisting}

Далее, функция - предикат areTypesCompatible возвращает значение True в случае, если первый тип может быть унифицирован вторым. 

\begin{lstlisting}

areTypesCompatible :: Type -> Type -> Bool  
areTypesCompatible Const          _              = True
areTypesCompatible TyVar{}        _              = True
areTypesCompatible (Arrow t1 t2) (Arrow t1' t2') = areTypesCompatible t1 t1' && areTypesCompatible t2 t2'
areTypesCompatible _             _               = False

\end{lstlisting}

Помимо этого была реализована подсистема строкового ввода-вывода термов и их типов.\\
В дополнение к основному алгоритму был реализован набор тестов, позволяющий проверять типы на небольшом колчистве термов. \\
Результат работы алгоритма:

\begin{lstlisting}

*Main> \x.\y.\z.xz(yz)

\x.\y.\z.xz(yz) :: (f -> e -> d) -> (f -> e) -> f -> d

*Main> k

\x.\y.x :: c -> b -> c

\end{lstlisting}

\hspace*{\fill} \\

\textbf{3. Определить условия, при которых имеет место эффект изменения типа.} \hspace*{\fill} \\
После реализации предыдущих двух алгоритмов, стал необходим метод, который принимает на вход терм и уровень логирования. Под логированием здесь понимается количество выводимых данных при обнаружение изменение наиболее общего типа. Очевидно, что getLogs должна иметь тип:

\begin{lstlisting}

getLogs : (Expr,String) -> (String)

\end{lstlisting}

К примеру,в результате получаем:
\begin{lstlisting}

*Main> getLogs (k, 1)

"Principal type did not change"

*Main> getLogs (threeminustwo, 1)

"Principal type changed"

\end{lstlisting}

\subsection{System F}

Аналогично предыдущему подразделу рассмотрим каждую задачу в отдельности.\\

\textbf{1. Реализовать систему пошаговой редукции.} \hspace*{\fill} \\

Как и для любой формальной системы для начала нам необходимо вспомнить определение в абстрактном синтаксисе(раздел 1.2):

\begin{center}

e := v|e_{1}e_{2}|$\lambda$x.e

\end{center}

\hspace*{\fill} \\

Теперь перепишем его в виде типа данных языка Haskell. 

\begin{lstlisting}

data Expr = Var String | App Expr Expr | Abs String Expr deriving (Eq, Ord)

\end{lstlisting}

Далее из раздела 1.1 следует что формально мы можем определить свободные переменные $\lambda$-выражения как\\

\begin{center}

FV(x) = \{x\} \\

FV(MN) = FV(M) $\cup$ FV(N) \\

FV($\lambda$x.M) = FV(M) $\setminus$ \{x\} 

\end{center} 

Вернемся к написанию кода: 

\begin{lstlisting}

occursFree :: Name -> Expr -> Bool 

occursFree x = foldExp (x==) (||) (\y r->x/=y && r) 

\end{lstlisting}

Данный метод осуществляет проверку принадлежности переменной x множеству свободных переменных.\\
Затем часто необходимо произвести замену соответствующих переменных. В разделе 1.1 были введены обозначения:

\begin{center}
M[x:=e] $\Leftrightarrow$ замене всех свободных вхождений x в M e.
\end{center}
Для углублённого изучения данного алгоритма можно порекомендовать работы [1] и [2].

Помним что при $\beta$-редукции выражение ($\lambda$x.M)N заменяется на M[x:=N], которое означает замещение всех свободных переменных x на N. 
Ниже приведен код для $\beta$-редукции. 

\begin{lstlisting}
beta :: Expr -> Expr -> Maybe Expr
beta (Abs x e) e2 = Just (subst e e2 x)
beta _         _  = Nothing
\end{lstlisting}

Как было показано в разделе 1, помимо этого нам необходимо уметь генерировать имена переменных, которые не используется в данный момент. 

\begin{lstlisting}
fresh :: Expr -> Name
fresh e = head (strings \\ ("":ids e)) 
    where strings  = "":[a:as | as <- strings, a <- ['a'..'z']]
\end{lstlisting}

Помимо этого была реализована подсистема строкового ввода-вывода термов.\\

\hspace*{\fill} \\

\textbf{2. Реализовать систему вывода типов.} \hspace*{\fill} \\

Так как было показано в [1] system F не всегда определить тип автоматически, поэтому необходимо сузить рассматриваемое множество, к примеру, для начала до System Fw.\\

В абстрактном синтаксисе имеем: \\

\begin{center}
unify (X, $\sigma$) = $\sigma$ \\
unify (Y, Y) = Y \\
unify ($\tau_{1}$ $\to$ $\tau_{2}$, $\sigma_{1}$ $\to$ $\sigma_{1}$) = unify($\tau_{1}$,$\sigma_{1}$) $\to$ unify($\tau_{2}$,$\sigma_{2}$) \\
unify ($\forall$Y.$\tau$(Y), $\forall$Y.$\sigma$(Y)) = $\forall$Y.unify($\tau$(Y),$\sigma$(Y)) (with Y a fresh variable) \\
unify (\_,\_) = raise Not\_unifiable \\
\end{center}

Теперь для решения наших проблем мы можем взять: \\
\begin{center}
f ($\Lambda$X.t) (r) = match type of t with "$\tau_{1}$ $\to$ $\tau_{2}$" => unify ($\tau_{1}$, type of r) | _ => fail end
\end{center}

Повторим вкарцее рассуждения предыдущего подраздела. \\
\hspace*{\fill} \\

\textbf{3. Определить условия, при которых имеет место эффект изменения типа.} \hspace*{\fill} \\
После реализации алгоритма Хинди-Миллера и редукции, аналогичным образом стал необходим метод, который принимает на вход терм и уровень логирования. Под логированием здесь понимается количество выводимых данных при обнаружение изменение наиболее общего типа. Очевидно, что getLogs должна иметь тип:

\begin{lstlisting}
getLogs : (Expr,String) -> (String)
\end{lstlisting}
\section{Выводы}

\subsection{Просто типизированное $\lambda$-исчисление}
После реализации алгоритмов из 3.1 были получены следующие результаты изменения наиболее общего типа:

\begin{itemize}
\item Когда при редукции одно из уравнений на типы исчезает.
\end{itemize}

Немного о полученом результате, данный результат вначале был замечен на практических примерах(к примеру при рассмотриении вычитании чисел Черча и примеры типа S K ->> $\x y. y$). Затем для обощения результата была сформулирована теорема, представленная ниже: \\

\textbf{Теорема.} Если при редукции происходит отбрасывание уравнения на типы с нетривиальной информацией, то возникает эффект изменения наиболее общего типа. \\
\textbf{Доказательство:} 
Если при редукции исчезает одно из уравнений на типы, следовательно при экспансии одно из уравнений на типы появиться. $\Rightarrow$
После экспансии получаем что система уравнений имеет ранг < количество неизвестных $\Rightarrow$ общее решение уравнения будет изменено $\Rightarrow$ Присвоенный тип будет изменен. \hspace*{\fill} \\
\textbf{ч.т.д.} 

\subsection{System F}

После реализации алгоритмов из 3.2 были получены соедующие результаты для наиболее общего типа.\\
Т.к. из определения $\lambda$-куба следует, что $\lambda$$\to$ \subsetneq System F. Следовательно, если эффект появляется в $\lambda$$\to$, то он будет появляться и в System F. Были получены следующие результаты:

\begin{enumerate}
\item Когда при редукции одно из уравнений на типы исчезает 
\item Были подтверждены некоторые теоритические результаты про наиболее общий тип из статьи [11].
\end{enumerate}
Первый результат очевиден из предыдущего подраздела и был подтвержден практически.(на таких примерах типа S K ->> $\x y. y$) 


%%% Local Variables: 


%%% TeX-master: "../thesis"

%%% End: 


